We give an optimal (EXPTIME), sound and complete tableau-based algorithm fordeciding satisfiability for propositional dynamic logic with converse (CPDL)which does not require the use of analytic cut. Our main contribution is asound methodto combine our previous optimal method for tracking leastfix-points in PDL with our previous optimal method for handling converse in thedescription logic ALCI. The extension is non-trivial as the two methods cannotbe combined naively. We give sufficient details to enable an implementation byothers. Our OCaml implementation seems to be the first theorem prover for CPDL.
展开▼
